Nuprl Definition : ecl-halt 11,40
ecl-halt(ds; da; x)
== ecl_ind(x;
== ecl_ind(k,test.(n,L. (n = 0)
== ecl_ind( (L':event-info(ds;da) List
== ecl_ind( (s:decl-state(ds)
== ecl_ind( (v:ma-valtype(da; k)
== ecl_ind( ((((L = append(L'; cons(<k, s, v>; [])))  ((test(s,v))))
== ecl_ind( ( l_all(L'; event-info(ds;da); t.(spreadn(t; k',s,v.((k = k') c ((test(s,v))))))
== ecl_ind( ( l_all())));
== ecl_ind(a,b,ha,hb.(n,L. ((0 < n)  (ha(n,L)))
== ecl_ind( (L1,L2:event-info(ds;da) List. ((L = append(L1; L2))  (ha(0,L1))  (hb(n,L2)))));
== ecl_ind(a,b,ha,hb.(n,L. ((n = 0)
== ecl_ind( (((ha(0,L))
== ecl_ind(  (L':event-info(ds;da) List. (iseg(event-info(ds;da); L'; L)  (hb(0,L')))))
== ecl_ind(  ((hb(0,L))
== ecl_ind(   (L':event-info(ds;da) List. (iseg(event-info(ds;da); L'; L)  (ha(0,L')))))))
== ecl_ind( ((0 < n)
== ecl_ind(  (((ha(n,L))
== ecl_ind(   (m:, L':(event-info(ds;da) List).
== ecl_ind(   iseg(event-info(ds;da); L'; L)  (hb(m,L'))  ((L' = L)  (n  m))))
== ecl_ind(   ((hb(n,L))
== ecl_ind(    (m:, L':(event-info(ds;da) List).
== ecl_ind(    iseg(event-info(ds;da); L'; L)  (ha(m,L'))  ((L' = L)  (n  m)))))));
== ecl_ind(a,b,ha,hb.(n,L. ((ha(n,L))
== ecl_ind( (m:, L':(event-info(ds;da) List).
== ecl_ind( iseg(event-info(ds;da); L'; L)  (hb(m,L'))  ((L' = L)  (n  m))))
== ecl_ind( ((hb(n,L))
== ecl_ind(  (m:, L':(event-info(ds;da) List).
== ecl_ind(  iseg(event-info(ds;da); L'; L)  (ha(m,L'))  ((L' = L)  (n  m)))));
== ecl_ind(a,ha.(n,L. (0 < n)  (star-append(event-info(ds;da); (ha(0)); (ha(n)))(L)));
== ecl_ind(a,m,ha.ha;
== ecl_ind(a,m,ha.(n,L. ((0 < n)  (ha(n,L)))  ((n = m)  (ha(0,L))));
== ecl_ind(a,l,ha.(n,L. ((ha(n,L))  ((n  l)))  ((n = 0)  l_exists(l; ; m.(ha(m,L)))))) 
latex

clarification:

ecl-halt(ds; da; x)
== ecl_ind(x;
== ecl_ind(k,test.(n,L. (n = 0  )
== ecl_ind( (L':event-info(ds;da) List
== ecl_ind( (s:decl-state(ds)
== ecl_ind( (v:ma-valtype(da; k)
== ecl_ind( ((((L = append(L'; cons(<k, s, v>; []))  (event-info(ds;da) List))
== ecl_ind( ( ((test(s,v))))
== ecl_ind( ( l_all(L';
== ecl_ind( ( l_all(event-info(ds;da);
== ecl_ind( ( l_all(t.(spreadn(t; k',s,v.((k = k'  Knd) c ((test(s,v))))))))));
== ecl_ind(a,b,ha,hb.(n,L. ((0 < n)  (ha(n,L)))
== ecl_ind( (L1:event-info(ds;da) List
== ecl_ind( (L2:event-info(ds;da) List
== ecl_ind( (((L = append(L1; L2)  (event-info(ds;da) List))  (ha(0,L1))  (hb(n,L2)))));
== ecl_ind(a,b,ha,hb.(n,L. ((n = 0  )
== ecl_ind( (((ha(0,L))
== ecl_ind(  (L':event-info(ds;da) List. (iseg(event-info(ds;da); L'; L)  (hb(0,L')))))
== ecl_ind(  ((hb(0,L))
== ecl_ind(   (L':event-info(ds;da) List. (iseg(event-info(ds;da); L'; L)  (ha(0,L')))))))
== ecl_ind( ((0 < n)
== ecl_ind(  (((ha(n,L))
== ecl_ind(   (m:, L':(event-info(ds;da) List).
== ecl_ind(   iseg(event-info(ds;da); L'; L)
== ecl_ind(    (hb(m,L'))
== ecl_ind(    ((L' = L  (event-info(ds;da) List))  (n  m))))
== ecl_ind(   ((hb(n,L))
== ecl_ind(    (m:, L':(event-info(ds;da) List).
== ecl_ind(    iseg(event-info(ds;da); L'; L)
== ecl_ind(     (ha(m,L'))
== ecl_ind(     ((L' = L  (event-info(ds;da) List))  (n  m)))))));
== ecl_ind(a,b,ha,hb.(n,L. ((ha(n,L))
== ecl_ind( (m:, L':(event-info(ds;da) List).
== ecl_ind( iseg(event-info(ds;da); L'; L)
== ecl_ind(  (hb(m,L'))
== ecl_ind(  ((L' = L  (event-info(ds;da) List))  (n  m))))
== ecl_ind( ((hb(n,L))
== ecl_ind(  (m:, L':(event-info(ds;da) List).
== ecl_ind(  iseg(event-info(ds;da); L'; L)
== ecl_ind(   (ha(m,L'))
== ecl_ind(   ((L' = L  (event-info(ds;da) List))  (n  m)))));
== ecl_ind(a,ha.(n,L. (0 < n)  (star-append(event-info(ds;da); (ha(0)); (ha(n)))(L)));
== ecl_ind(a,m,ha.ha;
== ecl_ind(a,m,ha.(n,L. ((0 < n)  (ha(n,L)))  ((n = m  )  (ha(0,L))));
== ecl_ind(a,l,ha.(n,L. ((ha(n,L))  ((n  l  )))  ((n = 0  )  l_exists(l; ; m.(ha(m,L)))))
== ecl_ind() 
latex

Definitionsf(a), , l_exists(L; T; x.P(x)), #$n, , s = t, P  Q, (x  l), A, P  Q, x.A(x), a < b, event-info(ds;da), star-append(T; P; Q), A  B, type List, P  Q, iseg(T; l1; l2), x:A. B(x), x:A. B(x), append(as; bs), b, Knd, A c B, spreadn(a; x,y,z.t(x;y;z)), l_all(L; T; x.P(x)), [], <a, b>, cons(car; cdr), ma-valtype(da; k), decl-state(ds), ecl ind
FDL editor aliasesecl-halt

origin